T:Type, R, R2:(TTProp).
Refl(T;_1,_2.R2(_1,_2))
 (Trans _1,_2:T. R2(_1,_2))
 (x, y:T. (x R y)  R2(x,y))
 (x, y:T. (x (R^*) y)  R2(x,y)) 

latex

Definitions	R^*, x f y, Trans x,y:T. E(x;y), Refl(T;x,y.E(x;y)), x,y. t(x;y), x(s1,s2), Prop, x:A. B(x), P  Q, t  T, P  Q
Lemmas	rel star closure, refl wf, trans wf, rel star wf